perm filename OTM.OLD[BMP,SYS]1 blob
sn#644369 filedate 1982-02-22 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00006 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 % old definition LTE
C00003 00003 % Measures for OTM operations -- 3-ary
C00006 00004 EVENTS.SINCE(GROUND.ZERO) 2FEB1982
C00010 00005 (SETQ FOO
C00014 00006 (viii) n ≤< m ∧ m ≤< p -> n ≤< p
C00016 ENDMK
C⊗;
% old definition LTE
DEFN(LTE (X Y)
(IF (OZEROP X) T
(IF (OZEROP Y) F
(IF (LTE (PA X) (PA Y))
(IF (LTE (PA Y) (PA X)) (LTE (PB X) (PB Y)) (LTE (PB X) Y))
(IF (LTE (PA Y) (PA X)) (LTE X (PB Y)) F) ))) )
% Measures for OTM operations -- 3-ary
DEFN(OTM.SIZE.3 (X Y Z) (PLUS (COUNT (OFIX X)) (COUNT (OFIX Y)) (COUNT (OFIX Z))))
PROVE.LEMMA(LT.PA.PA.PA (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)) (NOT (OZEROP Z))
(LESSP (OTM.SIZE.3 (PA X) (PA Y) (PA Z)) (OTM.SIZE.3 X Y Z))) )
PROVE.LEMMA(LT.PB.PB.PB (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y)) (NOT (OZEROP Z))
(LESSP (OTM.SIZE.3 (PB X) (PB Y) (PB Z)) (OTM.SIZE.3 X Y Z))) )
PROVE.LEMMA(LT.ID.PA.PA (INDUCTION)
(IMPLIES (OR (NOT (OZEROP Y)) (NOT (OZEROP Z))
(LESSP (OTM.SIZE.3 X (PA Y) (PA Z)) (OTM.SIZE.3 X Y Z))) )
PROVE.LEMMA(LT.PA.ID.PA (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Z))
(LESSP (OTM.SIZE.3 (PA X) Y (PA Z)) (OTM.SIZE.3 X Y Z))) )
PROVE.LEMMA(LT.PA.PA.ID (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))
(LESSP (OTM.SIZE.3 (PA X) (PA Y) Z) (OTM.SIZE.3 X Y Z))) )
PROVE.LEMMA(LT.ID.PB.PB (INDUCTION)
(IMPLIES (OR (NOT (OZEROP Y)) (NOT (OZEROP Z))
(LESSP (OTM.SIZE.3 X (PB Y) (PB Z)) (OTM.SIZE.3 X Y Z))) )
PROVE.LEMMA(LT.PB.ID.PB (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Z))
(LESSP (OTM.SIZE.3 (PB X) Y (PB Z)) (OTM.SIZE.3 X Y Z))) )
PROVE.LEMMA(LT.PB.PB.ID (INDUCTION)
(IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))
(LESSP (OTM.SIZE.3 (PB X) (PB Y) Z) (OTM.SIZE.3 X Y Z))) )
EVENTS.SINCE(GROUND.ZERO) 2FEB1982
((BOOT.STRAP) (ADD.SHELL PHI OZERO OTM ((PA (ONE.OF OTM) OZERO) (PB (
ONE.OF OTM) OZERO))) (DEFN OZEROP (X) (OR (EQUAL X (OZERO)) (NOT (OTM X)
))) (DEFN OFIX (X) (IF (OTM X) X (OZERO))) (DEFN OTM.SIZE.2 (X Y) (PLUS
(COUNT (OFIX X)) (COUNT (OFIX Y)))) (PROVE.LEMMA LT.PB.PB (INDUCTION) (
IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PB X)
(PB Y)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.PA (INDUCTION) (IMPLIES
(OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PA X) (PA Y))
(OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.PA.x (INDUCTION) (IMPLIES (OR (
NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PA Y) (PA X)) (
OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PB.ID (INDUCTION) (IMPLIES (NOT (
OZEROP X)) (LESSP (OTM.SIZE.2 (PB X) Y) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA
LT.ID.PB (INDUCTION) (IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PB
Y)) (OTM.SIZE.2 X Y)))) (DEFN LTE (X Y) (IF (OZEROP X) T (IF (OZEROP Y)
F (IF (LTE (PA X) (PA Y)) (IF (LTE (PA Y) (PA X)) (LTE (PB X) (PB Y)) (
LTE (PB X) Y)) (IF (LTE (PA Y) (PA X)) (LTE X (PB Y)) F))))) (DEFN LT (X
Y) (AND (LTE X Y) (NOT (LTE Y X)))) (DEFN EQ (X Y) (AND (LTE X Y) (LTE
Y X))) (PROVE.LEMMA LTE.BI (REWRITE) (IMPLIES (NOT (LTE X Y)) (LTE Y X))
) (PROVE.LEMMA LT.PA.ID (INDUCTION) (IMPLIES (NOT (OZEROP X)) (LESSP (
OTM.SIZE.2 (PA X) Y) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.ID.PA (
INDUCTION) (IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PA Y)) (
OTM.SIZE.2 X Y)))) (PROVE.LEMMA LTE.CASE.LTXY (REWRITE) (IMPLIES (AND (
NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA X) (PA Y))) (EQUAL (LTE X Y) (
LTE (PB X) Y)))) (PROVE.LEMMA LTE.CASE.EQXY (REWRITE) (IMPLIES (AND (NOT
(OZEROP X)) (NOT (OZEROP Y)) (EQ (PA X) (PA Y))) (EQUAL (LTE X Y) (LTE
(PB X) (PB Y))))) (PROVE.LEMMA LTE.CASE.LTYX (REWRITE) (IMPLIES (AND (
NOT (OZEROP X)) (NOT (OZEROP Y)) (LT (PA Y) (PA X))) (EQUAL (LTE X Y) (
LTE X (PB Y))))) (PROVE.LEMMA LT.CASE.LTXY (REWRITE) (IMPLIES (AND (NOT
(OZEROP X)) (NOT (OZEROP Y)) (LT (PA X) (PA Y))) (EQUAL (LT X Y) (LT (PB
X) Y)))) (PROVE.LEMMA LT.CASE.EQXY (REWRITE) (IMPLIES (AND (NOT (OZEROP
X)) (NOT (OZEROP Y)) (EQ (PA X) (PA Y))) (EQUAL (LT X Y) (LT (PB X) (PB
Y))))) (PROVE.LEMMA LT.CASE.LTYX (REWRITE) (IMPLIES (AND (NOT (OZEROP X
)) (NOT (OZEROP Y)) (LT (PA Y) (PA X))) (EQUAL (LT X Y) (LT X (PB Y)))))
)
31←
(SETQ FOO
'((BOOT.STRAP) (ADD.SHELL PHI OZERO OTM ((PA (ONE.OF OTM) OZERO) (PB (
ONE.OF OTM) OZERO))) (DEFN OZEROP (X) (OR (EQUAL X (OZERO)) (NOT (OTM X)
))) (DEFN OFIX (X) (IF (OTM X) X (OZERO))) (DEFN OTM.SIZE.2 (X Y) (PLUS
(COUNT (OFIX X)) (COUNT (OFIX Y)))) (PROVE.LEMMA LT.PB.PB (INDUCTION) (
IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PB X)
(PB Y)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PB.PB.x (INDUCTION) (
IMPLIES (OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PB Y)
(PB X)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.PA (INDUCTION) (IMPLIES
(OR (NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PA X) (PA Y))
(OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.PA.x (INDUCTION) (IMPLIES (OR (
NOT (OZEROP X)) (NOT (OZEROP Y))) (LESSP (OTM.SIZE.2 (PA Y) (PA X)) (
OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PA.ID (INDUCTION) (IMPLIES (NOT (
OZEROP X)) (LESSP (OTM.SIZE.2 (PA X) Y) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA
LT.PA.ID.x (INDUCTION) (IMPLIES (NOT (OZEROP X)) (LESSP (OTM.SIZE.2 Y (
PA X)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.PB.ID (INDUCTION) (IMPLIES (
NOT (OZEROP X)) (LESSP (OTM.SIZE.2 (PB X) Y) (OTM.SIZE.2 X Y)))) (
PROVE.LEMMA LT.PB.ID.x (INDUCTION) (IMPLIES (NOT (OZEROP X)) (LESSP (
OTM.SIZE.2 Y (PB X)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.ID.PA (
INDUCTION) (IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PA Y)) (
OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.ID.PA.x (INDUCTION) (IMPLIES (NOT (
OZEROP Y)) (LESSP (OTM.SIZE.2 (PA Y) X) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA
LT.ID.PB (INDUCTION) (IMPLIES (NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 X (PB
Y)) (OTM.SIZE.2 X Y)))) (PROVE.LEMMA LT.ID.PB.x (INDUCTION) (IMPLIES (
NOT (OZEROP Y)) (LESSP (OTM.SIZE.2 (PB Y) X) (OTM.SIZE.2 X Y)))) (DEFN
LTE (X Y) (IF (OZEROP X) T (IF (OZEROP Y) F (OR (AND (LTE (PA X) (PA Y))
(NOT (LTE (PA Y) (PA X))) (LTE (PB X) Y)) (AND (LTE (PA X) (PA Y)) (LTE
(PA Y) (PA X)) (LTE (PB X) (PB Y))) (AND (NOT (LTE (PA X) (PA Y))) (LTE
(PA Y) (PA X)) (LTE X (PB Y))))))) (PROVE.LEMMA OZERO.LTE.X NIL (LTE (
OZERO) X)) (PROVE.LEMMA X.LTE.OZERO NIL (IMPLIES (AND (OZEROP Y) (LTE X
Y)) (OZEROP X))) (DEFN LTE1 (X) (IF (OZEROP X) T (AND (LTE1 (PA X)) (
LTE1 (PB X))))) (PROVE.LEMMA LTE.XX (REWRITE) (EQUAL (LTE X X) (LTE1 X))
) (PROVE.LEMMA REFLEX.LTE NIL (LTE X X)) (PROVE.LEMMA TOTAL.LTE NIL (
IMPLIES (NOT (LTE X Y)) (LTE Y X)))) )
(viii) n ≤< m ∧ m ≤< p -> n ≤< p
PROVE.LEMMA(TRANS.LTE NIL (IMPLIES (AND (LTE X Y) (LTE Y Z)) (LTE X Z)) )
TRANS.LTE 0=0 Running at 330315 Used 0:16:41.7 in 0:51:38, Load 1.04
0=0 Running at 1003 Used 0:17:21.2 in 0:52:20, Load 1.03
0=0 Running at 12037 Used 0:18:21.7 in 0:53:24, Load 1.02
0=0 Running at 315763 Used 0:21:08.4 in 0:56:21, Load 1.05
0=0 Running at 25077 Used 0:22:35.4 in 0:57:53, Load 1.02
0=0 Running at 25077 Used 0:26:58.0 in 1:02:31, Load 1.02
***ERROR***
STORAGE FULL
0=0 Running at 30530 Used 0:28:02.0 in 1:03:38, Load 1.02
NIL
(ALL.PICKS broken)
11:
PROVE.LEMMA(TRANS.LTE NIL (IMPLIES (AND (LTE X Y) (LTE Y Z)) (LTE X Z)) )
PROVE.LEMMA(TRANS1.LTE NIL
(IMPLIES (AND (NOT (LTE X Z)) (LTE Y Z)) (NOT (LTE X Y))) )
PROVE.LEMMA(TRANS2.LTE NIL
(IMPLIES (AND (LTE X Y) (NOT (LTE X Z))) (NOT (LTE Y Z))) )